structure Proof2 =
struct
  structure A = Assert
  structure Asm = Assem
  
  type lemma = string
  type lab = string
  type asst_name = string

  datatype prf_blk
  (* prf_blk: the proof block of other instructions; 
   * asst_name: label of the postcondition 
   * lemma: if there is a vc-proof for some precise of this inference rule, then we can find the vc's name according to "lemma",
   *        orelse, lemma = ""
   *)
    = WF_addr of prf_blk * asst_name * lemma
    | WF_addz of prf_blk * asst_name * lemma
    | WF_subr of prf_blk * asst_name * lemma
    | WF_subz of prf_blk * asst_name * lemma
    | WF_mulr of prf_blk * asst_name * lemma
    | WF_mulz of prf_blk * asst_name * lemma
    | WF_push of prf_blk * asst_name * lemma
    | WF_pop of prf_blk * asst_name * lemma
    | WF_xchg of prf_blk * asst_name * lemma
    | WF_movr of prf_blk * asst_name * lemma
    | WF_movz of prf_blk * asst_name * lemma
    | WF_movld of prf_blk * asst_name * lemma
    | WF_movst of prf_blk * asst_name * lemma
    (* lab: the object that the instruction jump to. It is also the postcondition label of the jmp instruction *)
    | WF_bgt of lab * prf_blk * asst_name * lemma
    | WF_bge of lab * prf_blk * asst_name * lemma
    | WF_beq of lab * prf_blk * asst_name * lemma
    | WF_bgti of lab * prf_blk * asst_name * lemma
    | WF_beqi of lab * prf_blk * asst_name * lemma
    | WF_jmp of lab * lemma
    | WF_trivial


  datatype ptype
    = Int    (* Z *)
    | Label  (* label *)
    | Addr   (* Address *)
    | Hp     (* heap *)
    | Rf     (* register file *)
    | Sta    (* state *)
    | Reg    (* register *)
    | CB     (* code block *)
    | CT     (* code heap type *)
    | CH     (* code heap *)
    | Assert (* assertion *)
    | Prop of pterm  (* Proposition *)
    | Wild


  and pterm
    = Abs of (string * ptype) * pterm  (* abstraction, that is (arg_id, arg_type, function_body) *)
    | App of pterm * pterm  (* Application *)  
    | Var of string  (* variable *)
    | Ex of (string * ptype) * pterm (*exists*)

    | IntNum of int
    | Lab of int
    | AddrN of int 

    | ChTy of ((string * int) list)
    | Iseq of (Asm.instr list)
    | Ch of (Asm.instr list) list
    | Asst of string
    | St of pterm * pterm  (* (rf, hp) *)

    | True
    | Eax
    | Ebx
    | Ecx
    | Edx
    | Esi
    | Edi
    | Esp
    | Ebp

    | Plus of pterm * pterm (* e1 + e2 *)
    | Minus of pterm * pterm (* e1 - e2 *)
    | Times of pterm * pterm (* e1 * e2 *)

    | Gt of pterm * pterm  (* e1 > e2 *)
    | Ge of pterm * pterm  (* e1 >= e2 *)
    | Lt of pterm * pterm  (* e1 < e2 *)
    | Le of pterm * pterm  (* e1 <= e2 *)
    | Eq of pterm * pterm  (* e1 == e2 *)
    | Ne of pterm * pterm  (* e1 <> e2 *)

    | And of pterm * pterm  (* p1 /\ p2 *)
    | Or of pterm * pterm   (* p1 \/ p2 *)
    | Not of pterm (* ~p *)

  datatype tactic
    = T_apply of string * ((string * string) list)
    | T_exact of pterm
    | T_intros of (string list)
    | T_inversion_clear of string * (string list)
    | T_proof
    | T_qed
    | T_auto
    | T_unfold of string
    | T_or of tactic * tactic
    | T_seq of tactic * tactic
    | T_para of (tactic list)
    | T_split



end 
